Nuprl Definition : es-pplus 0,22

[e1,e2]~([a,b].p(a;b))+ == [e1;e2]~([a,b].p(a;b))*[a,b].p(a;b
latex



clarification:

es-pplus(es;a,b.p(a;b);e1;e2) == es-pstar-q(es;a,b.p(a;b);a,b.p(a;b);e1;e2
latex


Definitions[e1;e2]~([a,b].p(a;b))*[a,b].q(a;b)
FDL editor aliaseses-pplus

origin